Nuprl Definition : alle-at2
0,22
postcript
pdf
@
i
always.
P
(
x1
;
x2
) ==
e
@
i
.
P
(
x1
when
e
;
x2
when
e
)
latex
clarification:
alle-at2(
es
;
i
;
x1
;
x2
;
x1
,
x2
.
P
(
x1
;
x2
))
== alle-at(
es
;
i
;
e
.
P
(es-when(
es
;
x1
;
e
);es-when(
es
;
x2
;
e
)))
latex
Definitions
e
@
i
.
P
(
e
)
,
x
when
e
FDL editor aliases
alle-at2
origin
e@i. P(x1 when e;x2 when e)
e@i. P(x1 when e;x2 when e)
e@i. P(e)